help-page

How do you use LogicBox?

Create a new proof

Create a new proof by clicking on the ➕ icon on the front page. Then enter the name of the proof, and the type of logic the proof is in.

  • propositional logic: with atomic formulas and the logical connectives and
  • predicate logic: with quantifiers , predicates , functions and equality
  • arithmetic: with addition , multiplication , and .

13. create-proof.gif

(note: when a proof is created, it contains a single line with no formula or rule specified)

Add a line

Add a line to your proof by right-clicking on an existing step and clicking on ⬆️ to add a line above or on ⬇️ to add a line below.

01. add-line.gif

Enter a formula

Modify the formula of a line by double-clicking on it, and entering the new value.

02. edit-formula.gif

(alternatively, you can right-click and choose 'Edit')

Choose a rule

Choose a rule by clicking on the rule and selecting a new one from the side-panel. By hovering on a rule, you may see its definition.

03. choose-rule.gif

(note: when a new line is created, "???" is displayed to indicate no rule)

Pick lines to refer to

To refer to a line, click on a reference, then click on the line/box which you would like to refer to.

04. pick-refs.gif

Inspect errors

You may inspect the errors currently on a line/box by clicking on it, and viewing the errors in the side-panel.

05. inspect-single-line.gif

If no line/box is currently selected, the errors pertaining to the currently hovered element will be shown.

06. inspect-multiple-lines.gif

Add a box

Add a box to the proof by right-clicking on an existing step and clicking on ⬆️ to add a box above or on ⬇️ to add a box below.

07. add-box.gif

Remove a step

You may remove a line by right-clicking on it and selecting 'Delete'.

08. delete-line.gif

If you remove a box, you will remove all steps it contains.

09. delete-box.gif

Move a step

You can move a line/box by dragging it to its new location

10. move-line.gif

Edit fresh variable in a box (only in predicate logic/arithmetic)

You may add/edit a fresh variable by right-clicking on a box and choosing 'Edit fresh variable'.

11. edit-fresh-var-ctx-menu.gif

Alternatively you may double-click on the box to edit its fresh variable

12. edit-fresh-var-dbl-click.gif

Syntax

Propositional logic

Syntax
Propositional atoms , , , , ... a, b, p, q, ...
Conjunction (and) p and q, p A q, p ∧ q
Disjunction (or) a or b, a V b
Implication (if ... then) q implies r, q -> r, q => r
Negation (not) not s, !s, ¬s
Contradiction false, bot
Tautology true, top,

The following precedence rules apply (Huth, Micheal 1962, convention 1.3, page 5)

  • binds most tightly
  • then and , which are left-associative
  • then , which is right-associative

As examples, this means that

  • not p and q is parsed as
  • p and q or r is parsed as
  • p -> q -> r is parsed as

Note: if an ambiguous formula (such as p and q and r) is entered, it will automatically be converted to an unambiguous form (in this case )

Predicate logic

Syntax
Universal quantification (for all) forall x P(x), ∀x P(x)
Existensial quantification (exists) exists y Q(y), ∃y Q(y)
Predicate P(a, b, c)
Equality x = y
Variables , , , , x, y, z, x_0, k_{123}
Function application f(x, y, z)

The symbols are also supported, and are parsed as described above.

The following precedence rules apply (Huth, Micheal 1962, convention 2.4, page 101)

  • and bind most tightly
  • then and , which are left-associative
  • then , which is right-associative

As examples, this means that

  • forall x P(x) and not Q(x) is parsed as
  • P(a) and Q(b) or R(c) is parsed as
  • P(a) -> Q(b) -> R(c) is parsed as

Note: nullary predicates are also supported. As an example, this means that that the formula forall x S -> Q(x) ( ) consists of two predicate symbols , where takes arguments and takes .

Arithmetic

Syntax
Universal quantification (for all) forall x P(x), ∀x P(x)
Existensial quantification (exists) exists y Q(y), ∃y Q(y)
Equality x = y
Variables , , , , x, y, z, x_0, k_{123}
Addition (plus) x + y
Multiplication (times) x * y
Zero, One , 0, 1

As arithmetic is just an instance of predicate logic with no predicate symbols, the constants (or nullary functions) and functions (infix), the precedence rules described above still apply.